es:ES, ds:x:Id fp Type, da:k:Knd fp Type, i:Id.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  da(kind(e))?Top)
 (e:E. loc(e) = i  es-info(es;e)  event-info(ds;da)) 

latex

Definitions	ES, t  T, Id, Type, x. t(x), x:A. B(x), a:A fp B(a), Knd, Top, IdDeq, x.A(x), f(x)?z, vartype(i;x), x:AB(x), kind(e), KindDeq, valtype(e), loc(e), s = t, P  Q, E, Prop, State(ds), x:AB(x), val(e), state@i, (state when e), <a,b>, b, a = b, P  Q, P & Q, P  Q, {T}, es-info(es;e), event-info(ds;da)
Lemmas	all functionality wrt iff, implies functionality wrt iff, assert wf, eq id wf, subtype rel wf, assert-eq-id, es-state-when wf, subtype rel dep function, subtype rel self, es-val wf, decl-state wf, es-E wf, es-loc wf, es-valtype wf, Kind-deq wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, Knd wf, fpf wf, Id wf, event system wf